|
1: |
|
Term_sub(Case(m,xi,n),s) |
→ Frozen(m,Sum_sub(xi,s),n,s) |
2: |
|
Frozen(m,Sum_constant(Left),n,s) |
→ Term_sub(m,s) |
3: |
|
Frozen(m,Sum_constant(Right),n,s) |
→ Term_sub(n,s) |
4: |
|
Frozen(m,Sum_term_var(xi),n,s) |
→ Case(Term_sub(m,s),xi,Term_sub(n,s)) |
5: |
|
Term_sub(Term_app(m,n),s) |
→ Term_app(Term_sub(m,s),Term_sub(n,s)) |
6: |
|
Term_sub(Term_pair(m,n),s) |
→ Term_pair(Term_sub(m,s),Term_sub(n,s)) |
7: |
|
Term_sub(Term_inl(m),s) |
→ Term_inl(Term_sub(m,s)) |
8: |
|
Term_sub(Term_inr(m),s) |
→ Term_inr(Term_sub(m,s)) |
9: |
|
Term_sub(Term_var(x),Id) |
→ Term_var(x) |
10: |
|
Term_sub(Term_var(x),Cons_usual(y,m,s)) |
→ m |
11: |
|
Term_sub(Term_var(x),Cons_usual(y,m,s)) |
→ Term_sub(Term_var(x),s) |
12: |
|
Term_sub(Term_var(x),Cons_sum(xi,k,s)) |
→ Term_sub(Term_var(x),s) |
13: |
|
Term_sub(Term_sub(m,s),t) |
→ Term_sub(m,Concat(s,t)) |
14: |
|
Sum_sub(xi,Id) |
→ Sum_term_var(xi) |
15: |
|
Sum_sub(xi,Cons_sum(psi,k,s)) |
→ Sum_constant(k) |
16: |
|
Sum_sub(xi,Cons_sum(psi,k,s)) |
→ Sum_sub(xi,s) |
17: |
|
Sum_sub(xi,Cons_usual(y,m,s)) |
→ Sum_sub(xi,s) |
18: |
|
Concat(Concat(s,t),u) |
→ Concat(s,Concat(t,u)) |
19: |
|
Concat(Cons_usual(x,m,s),t) |
→ Cons_usual(x,Term_sub(m,t),Concat(s,t)) |
20: |
|
Concat(Cons_sum(xi,k,s),t) |
→ Cons_sum(xi,k,Concat(s,t)) |
21: |
|
Concat(Id,s) |
→ s |
|
There are 23 dependency pairs:
|
22: |
|
Term_sub#(Case(m,xi,n),s) |
→ Frozen#(m,Sum_sub(xi,s),n,s) |
23: |
|
Term_sub#(Case(m,xi,n),s) |
→ Sum_sub#(xi,s) |
24: |
|
Frozen#(m,Sum_constant(Left),n,s) |
→ Term_sub#(m,s) |
25: |
|
Frozen#(m,Sum_constant(Right),n,s) |
→ Term_sub#(n,s) |
26: |
|
Frozen#(m,Sum_term_var(xi),n,s) |
→ Term_sub#(m,s) |
27: |
|
Frozen#(m,Sum_term_var(xi),n,s) |
→ Term_sub#(n,s) |
28: |
|
Term_sub#(Term_app(m,n),s) |
→ Term_sub#(m,s) |
29: |
|
Term_sub#(Term_app(m,n),s) |
→ Term_sub#(n,s) |
30: |
|
Term_sub#(Term_pair(m,n),s) |
→ Term_sub#(m,s) |
31: |
|
Term_sub#(Term_pair(m,n),s) |
→ Term_sub#(n,s) |
32: |
|
Term_sub#(Term_inl(m),s) |
→ Term_sub#(m,s) |
33: |
|
Term_sub#(Term_inr(m),s) |
→ Term_sub#(m,s) |
34: |
|
Term_sub#(Term_var(x),Cons_usual(y,m,s)) |
→ Term_sub#(Term_var(x),s) |
35: |
|
Term_sub#(Term_var(x),Cons_sum(xi,k,s)) |
→ Term_sub#(Term_var(x),s) |
36: |
|
Term_sub#(Term_sub(m,s),t) |
→ Term_sub#(m,Concat(s,t)) |
37: |
|
Term_sub#(Term_sub(m,s),t) |
→ Concat#(s,t) |
38: |
|
Sum_sub#(xi,Cons_sum(psi,k,s)) |
→ Sum_sub#(xi,s) |
39: |
|
Sum_sub#(xi,Cons_usual(y,m,s)) |
→ Sum_sub#(xi,s) |
40: |
|
Concat#(Concat(s,t),u) |
→ Concat#(s,Concat(t,u)) |
41: |
|
Concat#(Concat(s,t),u) |
→ Concat#(t,u) |
42: |
|
Concat#(Cons_usual(x,m,s),t) |
→ Term_sub#(m,t) |
43: |
|
Concat#(Cons_usual(x,m,s),t) |
→ Concat#(s,t) |
44: |
|
Concat#(Cons_sum(xi,k,s),t) |
→ Concat#(s,t) |
|
The approximated dependency graph contains 3 SCCs:
{38,39},
{34,35}
and {22,24-33,36,37,40-44}.